Library cyclocevian_conjugate

Require Export PointsType.
Require Import complement.
Require Import isotomic_conjugate.
Require Import isogonal_conjugate.

Open Scope R_scope.

Section Triangle.

Context `{M:triangle_theory}.

Definition cyclocevian_conjugate P :=
  isotomic_conjugate
    (anticomplement
      (isogonal_conjugate
        (complement
          (isotomic_conjugate P)))).

End Triangle.